As hardware and software systems become more complex there is a growing need for mechanized formal verification methods. These methods are mathematically based techniques and languages that help detect and prevent design errors, thereby avoiding losses in design effort and financial investment.
One method for verifying properties of circuits and finite-state systems is known as Symbolic Trajectory Evaluation (STE). STE is an efficient model checking algorithm especially suited to verifying properties of large datapath designs (with thousands or tens of thousands of state encoding variables). In STE the Boolean data domain {0, 1} is extended to a partially-ordered state space including “don't care” values, X, for which their Boolean value is unknown.
One disadvantage associated with symbolic methods for verifying properties of circuits and finite state systems is known as state explosion. The state explosion problem is a failure characterized by exhaustion of computational resources because the required amount of computational resources expands (sometimes exponentially) according to the number of states defining the system.
A useful approach for reducing complexity in STE is called symbolic indexing. Symbolic indexing is a technique for formulating STE verification properties that exploit the partially ordered state space to use fewer state encoding variables, thereby reducing computation. One drawback has been that the process of manually encoding verification properties into indexed form may be tedious and prone to error. Another drawback has been that indexed verification results provide only an implied verification, which typically depends on some informal reasoning rather than explicit automated checks, and the indexed properties that are verified may not be directly applicable at higher levels of verification. There has also been no characterization of the conditions under which properties that are applicable at higher levels of verification can be derived from indexed properties. As a consequent, few practitioners have understood and mastered the techniques required to use symbolic indexing effectively.